p:FinProbSpace. Dec(Outcome) 

latex

Definitions	FinProbSpace, Dec(P), P  Q, A, Outcome, x:A. B(x), t  T, #$n
Lemmas	natural number wf p-outcome, p-outcome wf, not wf